Step of Proof: uni_sat_imp_in_uni_set 9,38
Inference at * 
Iof proof for Lemma uni sat imp in uni set:


  T:Type, a:T, Q:(T). (a = !x:T. Q(x))  (a  {!x:T | Q(x)}) 
latex
 by ((((Unfolds ``uni_sat unique_set`` 0) 
CollapseTHEN (RepD))) 
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 
latex

C1: 

C1: 1. T : Type
C1: 2. a : T
C1: 3. Q : T
C1: 4. Q(a)
C1: 5. a':T. Q(a')  (a' = a)
C1:   a  {x:T| Q(x)  (y:T. Q(y)  (y = x))} 
C.

DefinitionsP  Q, {!x:T | P(x)}, t  T, x(s), a = !x:T. Q(x), P  Q, , x:A. B(x)

origin